\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl(${\it ds}$;${\it da}$), $k$:Knd, $l$:IdLnk, ${\it tg}$:Id, $n$:$\mathbb{N}$,\+
\\[0ex]$f$:(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$${\it da}$(rcv($l$,${\it tg}$))?Void), ${\it es}$:ES.
\-\\[0ex](source($l$) = $i$)
\\[0ex]$\Rightarrow$ \=(@$i$[[$A$;$k$ sends on $l$ with tag ${\it tg}$ [$s$,$v$.$f$($s$,$v$)], at marker $n$]]\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)\+
\\[0ex]$\Rightarrow$ \=with decls \=${\it ds}$ \+\+
\\[0ex]${\it da}$
\-\\[0ex]sends on $l$ from $e$ 
\\[0ex]include \=if kind($e$) = $k$ $\wedge_{b}$ action[[$A$ $n$]][es{-}init(${\it es}$;$e$);$e$]\+
\\[0ex]then [$<$${\it tg}$, $f$((state when $e$),val($e$))$>$]
\\[0ex]else []
\\[0ex]fi  
\-\\[0ex]and only these for tags in [${\it tg}$]))
\-\-\-
\end{tabbing}